YES 8.153 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((group :: Eq a => [Maybe a]  ->  [[Maybe a]]) :: Eq a => [Maybe a]  ->  [[Maybe a]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = (\(ys,_) ->ys) vv10
zs = (\(_,zs) ->zs) vv10


module Maybe where
  import qualified List
import qualified Prelude


Lambda Reductions:
The following Lambda expression
\(_,zs)→zs

is transformed to
zs0 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys0 (ys,_) = ys

The following Lambda expression
\(_,zs)→zs

is transformed to
zs1 (_,zs) = zs

The following Lambda expression
\(ys,_)→ys

is transformed to
ys1 (ys,_) = ys



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR

mainModule List
  ((group :: Eq a => [Maybe a]  ->  [[Maybe a]]) :: Eq a => [Maybe a]  ->  [[Maybe a]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy _ [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,_) = ys
zs = zs0 vv10
zs0 (_,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)

is replaced by the following term
ww : wx



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR

mainModule List
  ((group :: Eq a => [Maybe a]  ->  [[Maybe a]]) :: Eq a => [Maybe a]  ->  [[Maybe a]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
span p [] = ([],[])
span p (ww : wx)
 | p ww
 = (ww : ys,zs)
 | otherwise
 = ([],ww : wx)
where 
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

is transformed to
span p [] = span3 p []
span p (ww : wx) = span2 p (ww : wx)

span2 p (ww : wx) = 
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

span3 p [] = ([],[])
span3 yz zu = span2 yz zu



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed

mainModule List
  ((group :: Eq a => [Maybe a]  ->  [[Maybe a]]) :: Eq a => [Maybe a]  ->  [[Maybe a]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = 
(x : ys) : groupBy eq zs where 
vv10 = span (eq x) xs
ys = ys0 vv10
ys0 (ys,vx) = ys
zs = zs0 vv10
zs0 (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs
where 
vv10  = span (eq x) xs
ys  = ys0 vv10
ys0 (ys,vx) = ys
zs  = zs0 vv10
zs0 (vy,zs) = zs

are unpacked to the following functions on top level
groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

groupByYs0 zv zw zx (ys,vx) = ys

groupByZs0 zv zw zx (vy,zs) = zs

groupByVv10 zv zw zx = span (zv zw) zx

The bindings of the following Let/Where expression
span1 p ww wx (p ww)
where 
span0 p ww wx True = ([],ww : wx)
span1 p ww wx True = (ww : ys,zs)
span1 p ww wx False = span0 p ww wx otherwise
vu43  = span p wx
ys  = ys1 vu43
ys1 (ys,wz) = ys
zs  = zs1 vu43
zs1 (wy,zs) = zs

are unpacked to the following functions on top level
span2Ys1 zy zz (ys,wz) = ys

span2Vu43 zy zz = span zy zz

span2Zs zy zz = span2Zs1 zy zz (span2Vu43 zy zz)

span2Span0 zy zz p ww wx True = ([],ww : wx)

span2Ys zy zz = span2Ys1 zy zz (span2Vu43 zy zz)

span2Span1 zy zz p ww wx True = (ww : span2Ys zy zz,span2Zs zy zz)
span2Span1 zy zz p ww wx False = span2Span0 zy zz p ww wx otherwise

span2Zs1 zy zz (wy,zs) = zs



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow

mainModule List
  (group :: Eq a => [Maybe a]  ->  [[Maybe a]])

module List where
  import qualified Maybe
import qualified Prelude
  group :: Eq a => [a]  ->  [[a]]
group = groupBy (==)

  groupBy :: (a  ->  a  ->  Bool)  ->  [a]  ->  [[a]]
groupBy vw [] = []
groupBy eq (x : xs) = (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs)

  
groupByVv10 zv zw zx = span (zv zw) zx

  
groupByYs zv zw zx = groupByYs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByYs0 zv zw zx (ys,vx) = ys

  
groupByZs zv zw zx = groupByZs0 zv zw zx (groupByVv10 zv zw zx)

  
groupByZs0 zv zw zx (vy,zs) = zs


module Maybe where
  import qualified List
import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vuu5300), Succ(vuu31001000)) → new_primPlusNat(vuu5300, vuu31001000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(vuu300100), Succ(vuu3100100)) → new_primMulNat(vuu300100, Succ(vuu3100100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat(vuu30000, vuu310000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(app(ty_@3, gd), ge), gf), gc) → new_esEs0(vuu3000, vuu31000, gd, ge, gf)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, app(app(ty_@2, ec), ed), cd) → new_esEs1(vuu3001, vuu31001, ec, ed)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, cc, app(app(ty_Either, fh), ga)) → new_esEs3(vuu3002, vuu31002, fh, ga)
new_esEs(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bb), bc), bd)) → new_esEs0(vuu3000, vuu31000, bb, bc, bd)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(app(ty_@3, bag), bah), bba)) → new_esEs0(vuu3000, vuu31000, bag, bah, bba)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_[], dc), cc, cd) → new_esEs2(vuu3000, vuu31000, dc)
new_esEs3(Right(vuu3000), Right(vuu31000), bdb, app(app(ty_Either, beb), bec)) → new_esEs3(vuu3000, vuu31000, beb, bec)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_[], ha), gc) → new_esEs2(vuu3000, vuu31000, ha)
new_esEs(Just(vuu3000), Just(vuu31000), app(ty_Maybe, ba)) → new_esEs(vuu3000, vuu31000, ba)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, app(app(app(ty_@3, dh), ea), eb), cd) → new_esEs0(vuu3001, vuu31001, dh, ea, eb)
new_esEs3(Right(vuu3000), Right(vuu31000), bdb, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs0(vuu3000, vuu31000, bdd, bde, bdf)
new_esEs3(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bch), bda), bca) → new_esEs3(vuu3000, vuu31000, bch, bda)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, app(ty_[], bac)) → new_esEs2(vuu3001, vuu31001, bac)
new_esEs3(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bcb), bcc), bcd), bca) → new_esEs0(vuu3000, vuu31000, bcb, bcc, bcd)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, app(app(ty_Either, bad), bae)) → new_esEs3(vuu3001, vuu31001, bad, bae)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, app(app(ty_@2, baa), bab)) → new_esEs1(vuu3001, vuu31001, baa, bab)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, cc, app(app(ty_@2, fd), ff)) → new_esEs1(vuu3002, vuu31002, fd, ff)
new_esEs3(Right(vuu3000), Right(vuu31000), bdb, app(ty_[], bea)) → new_esEs2(vuu3000, vuu31000, bea)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_@2, bbb), bbc)) → new_esEs1(vuu3000, vuu31000, bbb, bbc)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, app(ty_[], ee), cd) → new_esEs2(vuu3001, vuu31001, ee)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, cc, app(app(app(ty_@3, fa), fb), fc)) → new_esEs0(vuu3002, vuu31002, fa, fb, fc)
new_esEs3(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bce), bcf), bca) → new_esEs1(vuu3000, vuu31000, bce, bcf)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_Maybe, baf)) → new_esEs(vuu3000, vuu31000, baf)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bbg) → new_esEs2(vuu3001, vuu31001, bbg)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_Either, dd), de), cc, cd) → new_esEs3(vuu3000, vuu31000, dd, de)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_@2, gg), gh), gc) → new_esEs1(vuu3000, vuu31000, gg, gh)
new_esEs(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bh), ca)) → new_esEs3(vuu3000, vuu31000, bh, ca)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, cc, app(ty_[], fg)) → new_esEs2(vuu3002, vuu31002, fg)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_[], bbd)) → new_esEs2(vuu3000, vuu31000, bbd)
new_esEs3(Right(vuu3000), Right(vuu31000), bdb, app(ty_Maybe, bdc)) → new_esEs(vuu3000, vuu31000, bdc)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_Either, hb), hc), gc) → new_esEs3(vuu3000, vuu31000, hb, hc)
new_esEs(Just(vuu3000), Just(vuu31000), app(app(ty_@2, be), bf)) → new_esEs1(vuu3000, vuu31000, be, bf)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_@2, da), db), cc, cd) → new_esEs1(vuu3000, vuu31000, da, db)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, app(ty_Maybe, dg), cd) → new_esEs(vuu3001, vuu31001, dg)
new_esEs2(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_Either, bbe), bbf)) → new_esEs3(vuu3000, vuu31000, bbe, bbf)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_Maybe, gb), gc) → new_esEs(vuu3000, vuu31000, gb)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, app(ty_Maybe, he)) → new_esEs(vuu3001, vuu31001, he)
new_esEs3(Right(vuu3000), Right(vuu31000), bdb, app(app(ty_@2, bdg), bdh)) → new_esEs1(vuu3000, vuu31000, bdg, bdh)
new_esEs(Just(vuu3000), Just(vuu31000), app(ty_[], bg)) → new_esEs2(vuu3000, vuu31000, bg)
new_esEs3(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bbh), bca) → new_esEs(vuu3000, vuu31000, bbh)
new_esEs3(Left(vuu3000), Left(vuu31000), app(ty_[], bcg), bca) → new_esEs2(vuu3000, vuu31000, bcg)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, cc, app(ty_Maybe, eh)) → new_esEs(vuu3002, vuu31002, eh)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), df, app(app(ty_Either, ef), eg), cd) → new_esEs3(vuu3001, vuu31001, ef, eg)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_Maybe, cb), cc, cd) → new_esEs(vuu3000, vuu31000, cb)
new_esEs0(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(app(ty_@3, ce), cf), cg), cc, cd) → new_esEs0(vuu3000, vuu31000, ce, cf, cg)
new_esEs1(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), hd, app(app(app(ty_@3, hf), hg), hh)) → new_esEs0(vuu3001, vuu31001, hf, hg, hh)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPSizeChangeProof
                      ↳ QDP
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Zs1(vuu18, vuu200, vuu201, True, ba) → new_span2Zs(vuu18, vuu201, ba)
new_span2Zs1(vuu18, vuu200, vuu201, True, ba) → new_span2Ys(vuu18, vuu201, ba)
new_span2Ys1(vuu9, vuu110, vuu111, True, bb) → new_span2Zs(vuu9, vuu111, bb)
new_span2Ys(vuu9, :(vuu110, vuu111), bb) → new_span2Ys1(vuu9, vuu110, vuu111, new_esEs4(Just(vuu9), vuu110, bb), bb)
new_span2Ys1(vuu9, vuu110, vuu111, True, bb) → new_span2Ys(vuu9, vuu111, bb)
new_span2Zs(vuu18, :(vuu200, vuu201), ba) → new_span2Zs1(vuu18, vuu200, vuu201, new_esEs4(Just(vuu18), vuu200, ba), ba)

The TRS R consists of the following rules:

new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Maybe, beg)) → new_esEs4(vuu3000, vuu31000, beg)
new_esEs10(vuu3001, vuu31001, app(app(app(ty_@3, da), db), dc)) → new_esEs13(vuu3001, vuu31001, da, db, dc)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(ty_[], baa)) → new_esEs18(vuu3000, vuu31000, baa)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu5300), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu5300, vuu31001000)))
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_esEs17(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs14(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), bad) → new_asAs(new_esEs21(vuu3000, vuu31000, bad), new_esEs22(vuu3001, vuu31001, bad))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Nothing, bef) → False
new_esEs4(Nothing, Just(vuu31000), bef) → False
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bcb)) → new_esEs4(vuu3001, vuu31001, bcb)
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs15(EQ, EQ) → True
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bfc)) → new_esEs14(vuu3000, vuu31000, bfc)
new_esEs9(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_@2, cb), cc)) → new_esEs8(vuu3000, vuu31000, cb, cc)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs17(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(ty_Ratio, hf)) → new_esEs14(vuu3000, vuu31000, hf)
new_esEs18(:(vuu3000, vuu3001), :(vuu31000, vuu31001), eb) → new_asAs(new_esEs20(vuu3000, vuu31000, eb), new_esEs18(vuu3001, vuu31001, eb))
new_primMulNat0(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs12(vuu3002, vuu31002)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, ec)) → new_esEs4(vuu3000, vuu31000, ec)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_Either, gg), gh), ff) → new_esEs19(vuu3000, vuu31000, gg, gh)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs7(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Double, ff) → new_esEs6(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bah)) → new_esEs4(vuu3000, vuu31000, bah)
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, eg)) → new_esEs14(vuu3000, vuu31000, eg)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bdb), bdc)) → new_esEs19(vuu3001, vuu31001, bdb, bdc)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs5(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs13(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), bae, baf, bag) → new_asAs(new_esEs23(vuu3000, vuu31000, bae), new_asAs(new_esEs24(vuu3001, vuu31001, baf), new_esEs25(vuu3002, vuu31002, bag)))
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Ratio, gc), ff) → new_esEs14(vuu3000, vuu31000, gc)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs15(GT, LT) → False
new_esEs15(LT, GT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_[], cd)) → new_esEs18(vuu3000, vuu31000, cd)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Float, ff) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(Nothing, Nothing, bef) → True
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bcf)) → new_esEs14(vuu3001, vuu31001, bcf)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bfg), bfh)) → new_esEs19(vuu3000, vuu31000, bfg, bfh)
new_esEs10(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs18([], :(vuu31000, vuu31001), eb) → False
new_esEs18(:(vuu3000, vuu3001), [], eb) → False
new_esEs15(LT, LT) → True
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs11(@0, @0) → True
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs11(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, beh), bfa), bfb)) → new_esEs13(vuu3000, vuu31000, beh, bfa, bfb)
new_esEs12(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs10(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs16(True, True) → True
new_esEs10(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, bdh)) → new_esEs14(vuu3002, vuu31002, bdh)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bbe), bbf)) → new_esEs8(vuu3000, vuu31000, bbe, bbf)
new_esEs15(EQ, LT) → False
new_esEs15(LT, EQ) → False
new_esEs10(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, app(ty_[], fb)) → new_esEs18(vuu3000, vuu31000, fb)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(app(app(ty_@3, hc), hd), he)) → new_esEs13(vuu3000, vuu31000, hc, hd, he)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_Either, ce), cf)) → new_esEs19(vuu3000, vuu31000, ce, cf)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs16(vuu3002, vuu31002)
new_esEs15(GT, EQ) → False
new_esEs15(EQ, GT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(app(ty_Either, bab), bac)) → new_esEs19(vuu3000, vuu31000, bab, bac)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs9(vuu3000, vuu31000, app(ty_Ratio, ca)) → new_esEs14(vuu3000, vuu31000, ca)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bed), bee)) → new_esEs19(vuu3002, vuu31002, bed, bee)
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_asAs(False, vuu40) → False
new_primEqNat0(Zero, Zero) → True
new_esEs10(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Char, ff) → new_esEs17(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_esEs19(Left(vuu3000), Right(vuu31000), ha, ff) → False
new_esEs19(Right(vuu3000), Left(vuu31000), ha, ff) → False
new_esEs18([], [], eb) → True
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bbh), bca)) → new_esEs19(vuu3000, vuu31000, bbh, bca)
new_esEs25(vuu3002, vuu31002, app(ty_[], bec)) → new_esEs18(vuu3002, vuu31002, bec)
new_esEs10(vuu3001, vuu31001, app(app(ty_@2, de), df)) → new_esEs8(vuu3001, vuu31001, de, df)
new_esEs9(vuu3000, vuu31000, app(ty_Maybe, be)) → new_esEs4(vuu3000, vuu31000, be)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_[], bff)) → new_esEs18(vuu3000, vuu31000, bff)
new_esEs7(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, app(ty_[], bda)) → new_esEs18(vuu3001, vuu31001, bda)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs13(vuu3000, vuu31000, bba, bbb, bbc)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, eh), fa)) → new_esEs8(vuu3000, vuu31000, eh, fa)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Ordering, ff) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_primPlusNat0(Succ(vuu530), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu530, vuu3100100)))
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(app(ty_@2, hg), hh)) → new_esEs8(vuu3000, vuu31000, hg, hh)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_@0, ff) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs16(False, False) → True
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bde), bdf), bdg)) → new_esEs13(vuu3002, vuu31002, bde, bdf, bdg)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Maybe, fg), ff) → new_esEs4(vuu3000, vuu31000, fg)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_@2, gd), ge), ff) → new_esEs8(vuu3000, vuu31000, gd, ge)
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bea), beb)) → new_esEs8(vuu3002, vuu31002, bea, beb)
new_esEs8(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bc, bd) → new_asAs(new_esEs9(vuu3000, vuu31000, bc), new_esEs10(vuu3001, vuu31001, bd))
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Bool, ff) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(app(ty_@3, bf), bg), bh)) → new_esEs13(vuu3000, vuu31000, bf, bg, bh)
new_primPlusNat1(Succ(vuu5300), Zero) → Succ(vuu5300)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs10(vuu3001, vuu31001, app(ty_[], dg)) → new_esEs18(vuu3001, vuu31001, dg)
new_esEs9(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, fc), fd)) → new_esEs19(vuu3000, vuu31000, fc, fd)
new_esEs16(True, False) → False
new_esEs16(False, True) → False
new_esEs6(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs13(vuu3001, vuu31001, bcc, bcd, bce)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs10(vuu3001, vuu31001, app(app(ty_Either, dh), ea)) → new_esEs19(vuu3001, vuu31001, dh, ea)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, ed), ee), ef)) → new_esEs13(vuu3000, vuu31000, ed, ee, ef)
new_esEs10(vuu3001, vuu31001, app(ty_Ratio, dd)) → new_esEs14(vuu3001, vuu31001, dd)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Int, ff) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, fh), ga), gb), ff) → new_esEs13(vuu3000, vuu31000, fh, ga, gb)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_[], gf), ff) → new_esEs18(vuu3000, vuu31000, gf)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs6(vuu3002, vuu31002)
new_asAs(True, vuu40) → vuu40
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bdd)) → new_esEs4(vuu3002, vuu31002, bdd)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs5(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bcg), bch)) → new_esEs8(vuu3001, vuu31001, bcg, bch)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbd)) → new_esEs14(vuu3000, vuu31000, bbd)
new_esEs15(GT, GT) → True
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bbg)) → new_esEs18(vuu3000, vuu31000, bbg)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs15(vuu3002, vuu31002)
new_esEs9(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), ha, app(ty_Maybe, hb)) → new_esEs4(vuu3000, vuu31000, hb)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Integer, ff) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bfd), bfe)) → new_esEs8(vuu3000, vuu31000, bfd, bfe)
new_esEs10(vuu3001, vuu31001, app(ty_Maybe, cg)) → new_esEs4(vuu3001, vuu31001, cg)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True

The set Q consists of the following terms:

new_esEs9(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primMulNat0(Succ(x0), Zero)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs4(Nothing, Nothing, x0)
new_esEs20(x0, x1, ty_@0)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs22(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs11(@0, @0)
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Int)
new_esEs18([], :(x0, x1), x2)
new_esEs25(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_asAs(True, x0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs5(Integer(x0), Integer(x1))
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs4(Just(x0), Nothing, x1)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(False, True)
new_esEs16(True, False)
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs17(Char(x0), Char(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs21(x0, x1, ty_Int)
new_esEs16(True, True)
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs24(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs10(x0, x1, ty_Double)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Zero, Zero)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs9(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_primMulNat0(Zero, Zero)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Nothing, Just(x0), x1)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs10(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs18(:(x0, x1), [], x2)
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs9(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs10(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs24(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Ordering)
new_esEs9(x0, x1, ty_Ordering)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Double)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs20(x0, x1, ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs15(LT, LT)
new_esEs20(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs18([], [], x0)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_esEs6(Double(x0, x1), Double(x2, x3))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys0(:(vuu3110, vuu3111), ba) → new_span2Ys10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)
new_span2Zs0(:(vuu3110, vuu3111), ba) → new_span2Zs10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)

The TRS R consists of the following rules:

new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bef)) → new_esEs4(vuu3000, vuu31000, bef)
new_esEs10(vuu3001, vuu31001, app(app(app(ty_@3, cg), da), db)) → new_esEs13(vuu3001, vuu31001, cg, da, db)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(ty_[], hh)) → new_esEs18(vuu3000, vuu31000, hh)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu5300), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu5300, vuu31001000)))
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_esEs17(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs14(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), bac) → new_asAs(new_esEs21(vuu3000, vuu31000, bac), new_esEs22(vuu3001, vuu31001, bac))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Nothing, bee) → False
new_esEs4(Nothing, Just(vuu31000), bee) → False
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bca)) → new_esEs4(vuu3001, vuu31001, bca)
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs15(EQ, EQ) → True
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bfb)) → new_esEs14(vuu3000, vuu31000, bfb)
new_esEs9(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_@2, ca), cb)) → new_esEs8(vuu3000, vuu31000, ca, cb)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs17(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(ty_Ratio, he)) → new_esEs14(vuu3000, vuu31000, he)
new_esEs18(:(vuu3000, vuu3001), :(vuu31000, vuu31001), ea) → new_asAs(new_esEs20(vuu3000, vuu31000, ea), new_esEs18(vuu3001, vuu31001, ea))
new_primMulNat0(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs12(vuu3002, vuu31002)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, eb)) → new_esEs4(vuu3000, vuu31000, eb)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_Either, gf), gg), fd) → new_esEs19(vuu3000, vuu31000, gf, gg)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs7(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Double, fd) → new_esEs6(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bag)) → new_esEs4(vuu3000, vuu31000, bag)
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, ef)) → new_esEs14(vuu3000, vuu31000, ef)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bda), bdb)) → new_esEs19(vuu3001, vuu31001, bda, bdb)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs5(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs13(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), bad, bae, baf) → new_asAs(new_esEs23(vuu3000, vuu31000, bad), new_asAs(new_esEs24(vuu3001, vuu31001, bae), new_esEs25(vuu3002, vuu31002, baf)))
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Ratio, gb), fd) → new_esEs14(vuu3000, vuu31000, gb)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs15(GT, LT) → False
new_esEs15(LT, GT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_[], cc)) → new_esEs18(vuu3000, vuu31000, cc)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Float, fd) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs4(Nothing, Nothing, bee) → True
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bce)) → new_esEs14(vuu3001, vuu31001, bce)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bff), bfg)) → new_esEs19(vuu3000, vuu31000, bff, bfg)
new_esEs10(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs18([], :(vuu31000, vuu31001), ea) → False
new_esEs18(:(vuu3000, vuu3001), [], ea) → False
new_esEs15(LT, LT) → True
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs11(@0, @0) → True
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs11(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, beg), beh), bfa)) → new_esEs13(vuu3000, vuu31000, beg, beh, bfa)
new_esEs12(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs10(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs16(True, True) → True
new_esEs10(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, bdg)) → new_esEs14(vuu3002, vuu31002, bdg)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bbd), bbe)) → new_esEs8(vuu3000, vuu31000, bbd, bbe)
new_esEs15(EQ, LT) → False
new_esEs15(LT, EQ) → False
new_esEs10(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, app(ty_[], fa)) → new_esEs18(vuu3000, vuu31000, fa)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(app(app(ty_@3, hb), hc), hd)) → new_esEs13(vuu3000, vuu31000, hb, hc, hd)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_Either, cd), ce)) → new_esEs19(vuu3000, vuu31000, cd, ce)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs16(vuu3002, vuu31002)
new_esEs15(GT, EQ) → False
new_esEs15(EQ, GT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(app(ty_Either, baa), bab)) → new_esEs19(vuu3000, vuu31000, baa, bab)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs9(vuu3000, vuu31000, app(ty_Ratio, bh)) → new_esEs14(vuu3000, vuu31000, bh)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bec), bed)) → new_esEs19(vuu3002, vuu31002, bec, bed)
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_asAs(False, vuu40) → False
new_primEqNat0(Zero, Zero) → True
new_esEs10(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Char, fd) → new_esEs17(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_esEs19(Left(vuu3000), Right(vuu31000), gh, fd) → False
new_esEs19(Right(vuu3000), Left(vuu31000), gh, fd) → False
new_esEs18([], [], ea) → True
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bbg), bbh)) → new_esEs19(vuu3000, vuu31000, bbg, bbh)
new_esEs25(vuu3002, vuu31002, app(ty_[], beb)) → new_esEs18(vuu3002, vuu31002, beb)
new_esEs10(vuu3001, vuu31001, app(app(ty_@2, dd), de)) → new_esEs8(vuu3001, vuu31001, dd, de)
new_esEs9(vuu3000, vuu31000, app(ty_Maybe, bd)) → new_esEs4(vuu3000, vuu31000, bd)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_[], bfe)) → new_esEs18(vuu3000, vuu31000, bfe)
new_esEs7(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, app(ty_[], bch)) → new_esEs18(vuu3001, vuu31001, bch)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs13(vuu3000, vuu31000, bah, bba, bbb)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, eg), eh)) → new_esEs8(vuu3000, vuu31000, eg, eh)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Ordering, fd) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_primPlusNat0(Succ(vuu530), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu530, vuu3100100)))
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(app(ty_@2, hf), hg)) → new_esEs8(vuu3000, vuu31000, hf, hg)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_@0, fd) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs16(False, False) → True
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs13(vuu3002, vuu31002, bdd, bde, bdf)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Maybe, ff), fd) → new_esEs4(vuu3000, vuu31000, ff)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_@2, gc), gd), fd) → new_esEs8(vuu3000, vuu31000, gc, gd)
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bdh), bea)) → new_esEs8(vuu3002, vuu31002, bdh, bea)
new_esEs8(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bb, bc) → new_asAs(new_esEs9(vuu3000, vuu31000, bb), new_esEs10(vuu3001, vuu31001, bc))
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Bool, fd) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(app(ty_@3, be), bf), bg)) → new_esEs13(vuu3000, vuu31000, be, bf, bg)
new_primPlusNat1(Succ(vuu5300), Zero) → Succ(vuu5300)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs10(vuu3001, vuu31001, app(ty_[], df)) → new_esEs18(vuu3001, vuu31001, df)
new_esEs9(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, fb), fc)) → new_esEs19(vuu3000, vuu31000, fb, fc)
new_esEs16(True, False) → False
new_esEs16(False, True) → False
new_esEs6(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs13(vuu3001, vuu31001, bcb, bcc, bcd)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs10(vuu3001, vuu31001, app(app(ty_Either, dg), dh)) → new_esEs19(vuu3001, vuu31001, dg, dh)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, ec), ed), ee)) → new_esEs13(vuu3000, vuu31000, ec, ed, ee)
new_esEs10(vuu3001, vuu31001, app(ty_Ratio, dc)) → new_esEs14(vuu3001, vuu31001, dc)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Int, fd) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, fg), fh), ga), fd) → new_esEs13(vuu3000, vuu31000, fg, fh, ga)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_[], ge), fd) → new_esEs18(vuu3000, vuu31000, ge)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs6(vuu3002, vuu31002)
new_asAs(True, vuu40) → vuu40
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bdc)) → new_esEs4(vuu3002, vuu31002, bdc)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs5(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bcf), bcg)) → new_esEs8(vuu3001, vuu31001, bcf, bcg)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbc)) → new_esEs14(vuu3000, vuu31000, bbc)
new_esEs15(GT, GT) → True
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bbf)) → new_esEs18(vuu3000, vuu31000, bbf)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs15(vuu3002, vuu31002)
new_esEs9(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), gh, app(ty_Maybe, ha)) → new_esEs4(vuu3000, vuu31000, ha)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Integer, fd) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bfc), bfd)) → new_esEs8(vuu3000, vuu31000, bfc, bfd)
new_esEs10(vuu3001, vuu31001, app(ty_Maybe, cf)) → new_esEs4(vuu3001, vuu31001, cf)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True

The set Q consists of the following terms:

new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primMulNat0(Succ(x0), Zero)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqNat0(Zero, Succ(x0))
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs4(Nothing, Nothing, x0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(@0, @0)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs5(Integer(x0), Integer(x1))
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(False, True)
new_esEs16(True, False)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs4(Just(x0), Nothing, x1)
new_esEs17(Char(x0), Char(x1))
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs16(True, True)
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_esEs18(:(x0, x1), [], x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Double)
new_primEqNat0(Zero, Zero)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs18([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs9(x0, x1, ty_Integer)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1)
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, ty_Bool)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs9(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs10(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs15(LT, LT)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs18([], [], x0)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs6(Double(x0, x1), Double(x2, x3))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys0(:(vuu3110, vuu3111), ba) → new_span2Ys10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)
new_span2Zs0(:(vuu3110, vuu3111), ba) → new_span2Zs10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)

The TRS R consists of the following rules:

new_esEs4(Nothing, Just(vuu31000), bee) → False
new_esEs4(Nothing, Nothing, bee) → True

The set Q consists of the following terms:

new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primMulNat0(Succ(x0), Zero)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqNat0(Zero, Succ(x0))
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs4(Nothing, Nothing, x0)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(@0, @0)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs5(Integer(x0), Integer(x1))
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(False, True)
new_esEs16(True, False)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs4(Just(x0), Nothing, x1)
new_esEs17(Char(x0), Char(x1))
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs16(True, True)
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_esEs18(:(x0, x1), [], x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Double)
new_primEqNat0(Zero, Zero)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs18([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs9(x0, x1, ty_Integer)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1)
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs4(Just(x0), Just(x1), ty_Float)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, ty_Bool)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs9(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs10(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Nothing, Just(x0), x1)
new_esEs24(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs15(LT, LT)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs18([], [], x0)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs6(Double(x0, x1), Double(x2, x3))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primMulNat0(Succ(x0), Zero)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_esEs11(@0, @0)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Integer)
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_esEs5(Integer(x0), Integer(x1))
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(False, True)
new_esEs16(True, False)
new_esEs17(Char(x0), Char(x1))
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs16(True, True)
new_esEs24(x0, x1, ty_Integer)
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_esEs18(:(x0, x1), [], x2)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs10(x0, x1, ty_Double)
new_primEqNat0(Zero, Zero)
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs18([], :(x0, x1), x2)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs9(x0, x1, ty_Integer)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1)
new_esEs15(GT, LT)
new_esEs15(LT, GT)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primMulNat0(Zero, Zero)
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs25(x0, x1, ty_Bool)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs24(x0, x1, ty_@0)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_esEs10(x0, x1, ty_Bool)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs23(x0, x1, ty_Ordering)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs9(x0, x1, ty_Char)
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs10(x0, x1, ty_Float)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Double)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs25(x0, x1, ty_Ordering)
new_esEs20(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1, ty_Ordering)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs10(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Double)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs15(LT, LT)
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs20(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs18([], [], x0)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_esEs15(EQ, GT)
new_esEs15(GT, EQ)
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs6(Double(x0, x1), Double(x2, x3))



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ UsableRulesProof
                          ↳ QDP
                            ↳ QReductionProof
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_span2Ys0(:(vuu3110, vuu3111), ba) → new_span2Ys10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)
new_span2Zs10(vuu3110, vuu3111, True, ba) → new_span2Zs0(vuu3111, ba)
new_span2Zs0(:(vuu3110, vuu3111), ba) → new_span2Zs10(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Ys10(vuu3110, vuu3111, True, ba) → new_span2Ys0(vuu3111, ba)

The TRS R consists of the following rules:

new_esEs4(Nothing, Just(vuu31000), bee) → False
new_esEs4(Nothing, Nothing, bee) → True

The set Q consists of the following terms:

new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs4(Nothing, Nothing, x0)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs4(Just(x0), Nothing, x1)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs4(Nothing, Just(x0), x1)
new_esEs4(Just(x0), Just(x1), ty_@0)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)

The TRS R consists of the following rules:

new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Maybe, beh)) → new_esEs4(vuu3000, vuu31000, beh)
new_esEs10(vuu3001, vuu31001, app(app(app(ty_@3, db), dc), dd)) → new_esEs13(vuu3001, vuu31001, db, dc, dd)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_[], bag)) → new_esEs18(vuu3000, vuu31000, bag)
new_primPlusNat1(Succ(vuu5300), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu5300, vuu31001000)))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs17(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs14(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), ec) → new_asAs(new_esEs21(vuu3000, vuu31000, ec), new_esEs22(vuu3001, vuu31001, ec))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bcd)) → new_esEs4(vuu3001, vuu31001, bcd)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs4(Nothing, Just(vuu31000), ed) → False
new_esEs4(Just(vuu3000), Nothing, ed) → False
new_esEs15(EQ, EQ) → True
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs12(vuu300, vuu3100)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bfd)) → new_esEs14(vuu3000, vuu31000, bfd)
new_esEs9(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_@2, cc), cd)) → new_esEs8(vuu3000, vuu31000, cc, cd)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs17(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_Ratio, bad)) → new_esEs14(vuu3000, vuu31000, bad)
new_esEs18(:(vuu3000, vuu3001), :(vuu31000, vuu31001), eh) → new_asAs(new_esEs20(vuu3000, vuu31000, eh), new_esEs18(vuu3001, vuu31001, eh))
new_span2Zs11(vuu3110, vuu3111, True, ba) → new_span2Zs12(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_primMulNat0(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs12(vuu3002, vuu31002)
new_span2Ys3(vuu9, :(vuu110, vuu111), bb) → new_span2Ys14(vuu9, vuu110, vuu111, new_esEs4(Just(vuu9), vuu110, bb), bb)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs6(vuu300, vuu3100)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, fc)) → new_esEs4(vuu3000, vuu31000, fc)
new_esEs10(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_Either, hf), hg), fb) → new_esEs19(vuu3000, vuu31000, hf, hg)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs7(vuu3000, vuu31000)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, ec)) → new_esEs14(vuu300, vuu3100, ec)
new_span2Zs3(vuu18, [], bc) → []
new_span2Zs12(vuu3110, vuu3111, vuu48, vuu47, ba) → vuu47
new_groupByZs0(Nothing, :(Just(vuu3100), vuu311), ba) → :(Just(vuu3100), vuu311)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs7(vuu3002, vuu31002)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Double, fb) → new_esEs6(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bbb)) → new_esEs4(vuu3000, vuu31000, bbb)
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, fh)) → new_esEs14(vuu3000, vuu31000, fh)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bdd), bde)) → new_esEs19(vuu3001, vuu31001, bdd, bde)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_span2Zs3(vuu18, :(vuu200, vuu201), bc) → new_span2Zs14(vuu18, vuu200, vuu201, new_esEs4(Just(vuu18), vuu200, bc), bc)
new_esEs5(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs13(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), ee, ef, eg) → new_asAs(new_esEs23(vuu3000, vuu31000, ee), new_asAs(new_esEs24(vuu3001, vuu31001, ef), new_esEs25(vuu3002, vuu31002, eg)))
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Ratio, hb), fb) → new_esEs14(vuu3000, vuu31000, hb)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, ed)) → new_esEs4(vuu300, vuu3100, ed)
new_esEs9(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Float, fb) → new_esEs12(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_[], ce)) → new_esEs18(vuu3000, vuu31000, ce)
new_span2Zs14(vuu18, vuu200, vuu201, False, bc) → :(vuu200, vuu201)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bch)) → new_esEs14(vuu3001, vuu31001, bch)
new_esEs4(Nothing, Nothing, ed) → True
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bfh), bga)) → new_esEs19(vuu3000, vuu31000, bfh, bga)
new_esEs10(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, bd), be)) → new_esEs8(vuu300, vuu3100, bd, be)
new_esEs18([], :(vuu31000, vuu31001), eh) → False
new_esEs18(:(vuu3000, vuu3001), [], eh) → False
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs15(LT, LT) → True
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, ee), ef), eg)) → new_esEs13(vuu300, vuu3100, ee, ef, eg)
new_esEs11(@0, @0) → True
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs11(vuu3002, vuu31002)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bfa), bfb), bfc)) → new_esEs13(vuu3000, vuu31000, bfa, bfb, bfc)
new_span2Ys12(vuu3110, vuu3111, True, ba) → new_span2Ys13(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_span2Zs14(vuu18, vuu200, vuu201, True, bc) → new_span2Zs13(vuu18, vuu200, vuu201, new_span2Ys3(vuu18, vuu201, bc), new_span2Zs3(vuu18, vuu201, bc), bc)
new_esEs12(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs10(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_span2Ys13(vuu3110, vuu3111, vuu46, vuu45, ba) → :(vuu3110, vuu46)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs15(vuu300, vuu3100)
new_groupByZs00(vuu18, vuu19, vuu20, True, bc) → new_span2Zs3(vuu18, vuu20, bc)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs16(True, True) → True
new_esEs10(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, beb)) → new_esEs14(vuu3002, vuu31002, beb)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bbg), bbh)) → new_esEs8(vuu3000, vuu31000, bbg, bbh)
new_esEs10(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs20(vuu3000, vuu31000, app(ty_[], gc)) → new_esEs18(vuu3000, vuu31000, gc)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(app(ty_@3, baa), bab), bac)) → new_esEs13(vuu3000, vuu31000, baa, bab, bac)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_Either, cf), cg)) → new_esEs19(vuu3000, vuu31000, cf, cg)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs16(vuu3002, vuu31002)
new_span2Ys11(vuu9, vuu110, vuu111, vuu50, vuu49, bb) → :(vuu110, vuu50)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(ty_Either, bah), bba)) → new_esEs19(vuu3000, vuu31000, bah, bba)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_groupByZs0(vuu30, [], ba) → []
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_Ratio, cb)) → new_esEs14(vuu3000, vuu31000, cb)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bef), beg)) → new_esEs19(vuu3002, vuu31002, bef, beg)
new_asAs(False, vuu40) → False
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_groupByZs0(Nothing, :(Nothing, vuu311), ba) → new_span2Zs2(vuu311, ba)
new_primEqNat0(Zero, Zero) → True
new_esEs10(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Char, fb) → new_esEs17(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_esEs19(Right(vuu3000), Left(vuu31000), fa, fb) → False
new_esEs19(Left(vuu3000), Right(vuu31000), fa, fb) → False
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs17(vuu300, vuu3100)
new_esEs18([], [], eh) → True
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bcb), bcc)) → new_esEs19(vuu3000, vuu31000, bcb, bcc)
new_esEs25(vuu3002, vuu31002, app(ty_[], bee)) → new_esEs18(vuu3002, vuu31002, bee)
new_esEs10(vuu3001, vuu31001, app(app(ty_@2, df), dg)) → new_esEs8(vuu3001, vuu31001, df, dg)
new_esEs9(vuu3000, vuu31000, app(ty_Maybe, bf)) → new_esEs4(vuu3000, vuu31000, bf)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_[], bfg)) → new_esEs18(vuu3000, vuu31000, bfg)
new_esEs7(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, app(ty_[], bdc)) → new_esEs18(vuu3001, vuu31001, bdc)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs13(vuu3000, vuu31000, bbc, bbd, bbe)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, ga), gb)) → new_esEs8(vuu3000, vuu31000, ga, gb)
new_span2Zs2(:(vuu3110, vuu3111), ba) → new_span2Zs11(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs16(vuu300, vuu3100)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Ordering, fb) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs7(vuu300, vuu3100)
new_span2Ys12(vuu3110, vuu3111, False, ba) → []
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs5(vuu300, vuu3100)
new_esEs10(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_primPlusNat0(Succ(vuu530), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu530, vuu3100100)))
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(ty_@2, bae), baf)) → new_esEs8(vuu3000, vuu31000, bae, baf)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_@0, fb) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_span2Zs11(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_esEs16(False, False) → True
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs13(vuu3002, vuu31002, bdg, bdh, bea)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_@2, hc), hd), fb) → new_esEs8(vuu3000, vuu31000, hc, hd)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Maybe, gf), fb) → new_esEs4(vuu3000, vuu31000, gf)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, fa), fb)) → new_esEs19(vuu300, vuu3100, fa, fb)
new_esEs8(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bd, be) → new_asAs(new_esEs9(vuu3000, vuu31000, bd), new_esEs10(vuu3001, vuu31001, be))
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bec), bed)) → new_esEs8(vuu3002, vuu31002, bec, bed)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Bool, fb) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(app(ty_@3, bg), bh), ca)) → new_esEs13(vuu3000, vuu31000, bg, bh, ca)
new_primPlusNat1(Succ(vuu5300), Zero) → Succ(vuu5300)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs10(vuu3001, vuu31001, app(ty_[], dh)) → new_esEs18(vuu3001, vuu31001, dh)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, gd), ge)) → new_esEs19(vuu3000, vuu31000, gd, ge)
new_esEs9(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs16(False, True) → False
new_esEs16(True, False) → False
new_span2Zs2([], ba) → []
new_esEs6(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_span2Ys14(vuu9, vuu110, vuu111, True, bb) → new_span2Ys11(vuu9, vuu110, vuu111, new_span2Ys3(vuu9, vuu111, bb), new_span2Zs3(vuu9, vuu111, bb), bb)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs13(vuu3001, vuu31001, bce, bcf, bcg)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_esEs10(vuu3001, vuu31001, app(app(ty_Either, ea), eb)) → new_esEs19(vuu3001, vuu31001, ea, eb)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, fd), ff), fg)) → new_esEs13(vuu3000, vuu31000, fd, ff, fg)
new_esEs10(vuu3001, vuu31001, app(ty_Ratio, de)) → new_esEs14(vuu3001, vuu31001, de)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Int, fb) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_[], he), fb) → new_esEs18(vuu3000, vuu31000, he)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, gg), gh), ha), fb) → new_esEs13(vuu3000, vuu31000, gg, gh, ha)
new_esEs26(vuu300, vuu3100, app(ty_[], eh)) → new_esEs18(vuu300, vuu3100, eh)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs6(vuu3002, vuu31002)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs11(vuu300, vuu3100)
new_span2Ys3(vuu9, [], bb) → []
new_span2Ys2([], ba) → []
new_asAs(True, vuu40) → vuu40
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bdf)) → new_esEs4(vuu3002, vuu31002, bdf)
new_groupByZs0(Just(vuu300), :(Just(vuu3100), vuu311), ba) → new_groupByZs00(vuu300, vuu3100, vuu311, new_esEs26(vuu300, vuu3100, ba), ba)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs5(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bda), bdb)) → new_esEs8(vuu3001, vuu31001, bda, bdb)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbf)) → new_esEs14(vuu3000, vuu31000, bbf)
new_span2Ys2(:(vuu3110, vuu3111), ba) → new_span2Ys12(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_esEs15(GT, GT) → True
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bca)) → new_esEs18(vuu3000, vuu31000, bca)
new_esEs9(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs15(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_Maybe, hh)) → new_esEs4(vuu3000, vuu31000, hh)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Integer, fb) → new_esEs5(vuu3000, vuu31000)
new_span2Ys14(vuu9, vuu110, vuu111, False, bb) → []
new_span2Zs13(vuu18, vuu200, vuu201, vuu52, vuu51, bc) → vuu51
new_groupByZs00(vuu18, vuu19, vuu20, False, bc) → :(Just(vuu19), vuu20)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bfe), bff)) → new_esEs8(vuu3000, vuu31000, bfe, bff)
new_esEs10(vuu3001, vuu31001, app(ty_Maybe, da)) → new_esEs4(vuu3001, vuu31001, da)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_groupByZs0(Just(vuu300), :(Nothing, vuu311), ba) → :(Nothing, vuu311)

The set Q consists of the following terms:

new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs9(x0, x1, ty_Bool)
new_esEs18(:(x0, x1), [], x2)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_span2Ys3(x0, [], x1)
new_primMulNat0(Succ(x0), Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs18([], [], x0)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_span2Zs11(x0, x1, True, x2)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, x4, x5)
new_groupByZs0(x0, [], x1)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_groupByZs0(Nothing, :(Nothing, x0), x1)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(@0, @0)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_esEs10(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Integer(x0), Integer(x1))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Zs11(x0, x1, False, x2)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_span2Ys12(x0, x1, False, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Double)
new_span2Ys3(x0, :(x1, x2), x3)
new_esEs16(True, False)
new_esEs16(False, True)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs17(Char(x0), Char(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_span2Ys14(x0, x1, x2, True, x3)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_span2Ys12(x0, x1, True, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs16(True, True)
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_groupByZs0(Just(x0), :(Just(x1), x2), x3)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_span2Zs2([], x0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs10(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_primEqNat0(Zero, Zero)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_span2Zs13(x0, x1, x2, x3, x4, x5)
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_span2Ys2(:(x0, x1), x2)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs9(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_span2Ys2([], x0)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_groupByZs00(x0, x1, x2, False, x3)
new_primMulNat0(Zero, Zero)
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Bool)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_groupByZs0(Just(x0), :(Nothing, x1), x2)
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_span2Zs14(x0, x1, x2, True, x3)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_@0)
new_esEs4(Just(x0), Nothing, x1)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_span2Ys13(x0, x1, x2, x3, x4)
new_esEs23(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_span2Ys14(x0, x1, x2, False, x3)
new_esEs10(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_groupByZs00(x0, x1, x2, True, x3)
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs12(x0, x1, x2, x3, x4)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs18([], :(x0, x1), x2)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_span2Zs2(:(x0, x1), x2)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Double)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs9(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_span2Zs14(x0, x1, x2, False, x3)
new_esEs23(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_groupByZs0(Nothing, :(Just(x0), x1), x2)
new_esEs15(LT, LT)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_span2Zs3(x0, :(x1, x2), x3)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_span2Zs3(x0, [], x1)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Double(x0, x1), Double(x2, x3))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x1, x2)) = 1 + x2   
POL(:%(x1, x2)) = 0   
POL(@0) = 0   
POL(@2(x1, x2)) = 0   
POL(@3(x1, x2, x3)) = 0   
POL(Char(x1)) = 0   
POL(Double(x1, x2)) = 0   
POL(EQ) = 0   
POL(False) = 0   
POL(Float(x1, x2)) = 0   
POL(GT) = 0   
POL(Integer(x1)) = 0   
POL(Just(x1)) = 0   
POL(LT) = 0   
POL(Left(x1)) = 0   
POL(Neg(x1)) = 0   
POL(Nothing) = 0   
POL(Pos(x1)) = 0   
POL(Right(x1)) = 0   
POL(Succ(x1)) = 0   
POL(True) = 0   
POL(Zero) = 0   
POL([]) = 0   
POL(app(x1, x2)) = 0   
POL(new_asAs(x1, x2)) = 0   
POL(new_esEs10(x1, x2, x3)) = x3   
POL(new_esEs11(x1, x2)) = 0   
POL(new_esEs12(x1, x2)) = 0   
POL(new_esEs13(x1, x2, x3, x4, x5)) = 0   
POL(new_esEs14(x1, x2, x3)) = 0   
POL(new_esEs15(x1, x2)) = 0   
POL(new_esEs16(x1, x2)) = 0   
POL(new_esEs17(x1, x2)) = 0   
POL(new_esEs18(x1, x2, x3)) = 0   
POL(new_esEs19(x1, x2, x3, x4)) = 0   
POL(new_esEs20(x1, x2, x3)) = 0   
POL(new_esEs21(x1, x2, x3)) = 0   
POL(new_esEs22(x1, x2, x3)) = 0   
POL(new_esEs23(x1, x2, x3)) = 0   
POL(new_esEs24(x1, x2, x3)) = 0   
POL(new_esEs25(x1, x2, x3)) = x1 + x3   
POL(new_esEs26(x1, x2, x3)) = x3   
POL(new_esEs4(x1, x2, x3)) = 0   
POL(new_esEs5(x1, x2)) = 0   
POL(new_esEs6(x1, x2)) = 0   
POL(new_esEs7(x1, x2)) = 0   
POL(new_esEs8(x1, x2, x3, x4)) = 0   
POL(new_esEs9(x1, x2, x3)) = 0   
POL(new_groupBy(x1, x2)) = x1   
POL(new_groupByZs0(x1, x2, x3)) = x2   
POL(new_groupByZs00(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_primEqInt(x1, x2)) = 0   
POL(new_primEqNat0(x1, x2)) = 0   
POL(new_primMulNat0(x1, x2)) = 0   
POL(new_primPlusNat0(x1, x2)) = 0   
POL(new_primPlusNat1(x1, x2)) = 1   
POL(new_span2Ys11(x1, x2, x3, x4, x5, x6)) = 1 + x4   
POL(new_span2Ys12(x1, x2, x3, x4)) = 1 + x2   
POL(new_span2Ys13(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys14(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Ys2(x1, x2)) = x1   
POL(new_span2Ys3(x1, x2, x3)) = x2   
POL(new_span2Zs11(x1, x2, x3, x4)) = 1 + x2   
POL(new_span2Zs12(x1, x2, x3, x4, x5)) = x4   
POL(new_span2Zs13(x1, x2, x3, x4, x5, x6)) = x5   
POL(new_span2Zs14(x1, x2, x3, x4, x5)) = 1 + x3   
POL(new_span2Zs2(x1, x2)) = x1   
POL(new_span2Zs3(x1, x2, x3)) = x2   
POL(new_sr(x1, x2)) = 0   
POL(ty_@0) = 0   
POL(ty_@2) = 0   
POL(ty_@3) = 0   
POL(ty_Bool) = 0   
POL(ty_Char) = 0   
POL(ty_Double) = 1   
POL(ty_Either) = 0   
POL(ty_Float) = 0   
POL(ty_Int) = 0   
POL(ty_Integer) = 0   
POL(ty_Maybe) = 0   
POL(ty_Ordering) = 0   
POL(ty_Ratio) = 0   
POL(ty_[]) = 0   

The following usable rules [17] were oriented:

new_span2Zs11(vuu3110, vuu3111, True, ba) → new_span2Zs12(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_span2Zs14(vuu18, vuu200, vuu201, True, bc) → new_span2Zs13(vuu18, vuu200, vuu201, new_span2Ys3(vuu18, vuu201, bc), new_span2Zs3(vuu18, vuu201, bc), bc)
new_span2Ys12(vuu3110, vuu3111, True, ba) → new_span2Ys13(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_groupByZs0(Nothing, :(Nothing, vuu311), ba) → new_span2Zs2(vuu311, ba)
new_span2Ys3(vuu9, :(vuu110, vuu111), bb) → new_span2Ys14(vuu9, vuu110, vuu111, new_esEs4(Just(vuu9), vuu110, bb), bb)
new_span2Zs11(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_span2Zs2(:(vuu3110, vuu3111), ba) → new_span2Zs11(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_groupByZs0(Just(vuu300), :(Nothing, vuu311), ba) → :(Nothing, vuu311)
new_span2Ys12(vuu3110, vuu3111, False, ba) → []
new_span2Ys14(vuu9, vuu110, vuu111, True, bb) → new_span2Ys11(vuu9, vuu110, vuu111, new_span2Ys3(vuu9, vuu111, bb), new_span2Zs3(vuu9, vuu111, bb), bb)
new_groupByZs0(Nothing, :(Just(vuu3100), vuu311), ba) → :(Just(vuu3100), vuu311)
new_span2Ys11(vuu9, vuu110, vuu111, vuu50, vuu49, bb) → :(vuu110, vuu50)
new_span2Ys3(vuu9, [], bb) → []
new_span2Zs14(vuu18, vuu200, vuu201, False, bc) → :(vuu200, vuu201)
new_span2Ys13(vuu3110, vuu3111, vuu46, vuu45, ba) → :(vuu3110, vuu46)
new_groupByZs00(vuu18, vuu19, vuu20, True, bc) → new_span2Zs3(vuu18, vuu20, bc)
new_groupByZs00(vuu18, vuu19, vuu20, False, bc) → :(Just(vuu19), vuu20)
new_groupByZs0(Just(vuu300), :(Just(vuu3100), vuu311), ba) → new_groupByZs00(vuu300, vuu3100, vuu311, new_esEs26(vuu300, vuu3100, ba), ba)
new_span2Zs13(vuu18, vuu200, vuu201, vuu52, vuu51, bc) → vuu51
new_span2Zs2([], ba) → []
new_span2Zs3(vuu18, [], bc) → []
new_groupByZs0(vuu30, [], ba) → []
new_span2Zs12(vuu3110, vuu3111, vuu48, vuu47, ba) → vuu47
new_span2Ys14(vuu9, vuu110, vuu111, False, bb) → []
new_span2Ys2(:(vuu3110, vuu3111), ba) → new_span2Ys12(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_span2Zs3(vuu18, :(vuu200, vuu201), bc) → new_span2Zs14(vuu18, vuu200, vuu201, new_esEs4(Just(vuu18), vuu200, bc), bc)
new_span2Ys2([], ba) → []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ LetRed
                ↳ HASKELL
                  ↳ Narrow
                    ↳ AND
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                      ↳ QDP
                        ↳ QDPOrderProof
                          ↳ QDP
                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Maybe, beh)) → new_esEs4(vuu3000, vuu31000, beh)
new_esEs10(vuu3001, vuu31001, app(app(app(ty_@3, db), dc), dd)) → new_esEs13(vuu3001, vuu31001, db, dc, dd)
new_esEs24(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_[], bag)) → new_esEs18(vuu3000, vuu31000, bag)
new_primPlusNat1(Succ(vuu5300), Succ(vuu31001000)) → Succ(Succ(new_primPlusNat1(vuu5300, vuu31001000)))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs17(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs14(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), ec) → new_asAs(new_esEs21(vuu3000, vuu31000, ec), new_esEs22(vuu3001, vuu31001, ec))
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(ty_Maybe, bcd)) → new_esEs4(vuu3001, vuu31001, bcd)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_esEs21(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs4(Nothing, Just(vuu31000), ed) → False
new_esEs4(Just(vuu3000), Nothing, ed) → False
new_esEs15(EQ, EQ) → True
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs12(vuu300, vuu3100)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bfd)) → new_esEs14(vuu3000, vuu31000, bfd)
new_esEs9(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_@2, cc), cd)) → new_esEs8(vuu3000, vuu31000, cc, cd)
new_esEs25(vuu3002, vuu31002, ty_Char) → new_esEs17(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_Ratio, bad)) → new_esEs14(vuu3000, vuu31000, bad)
new_esEs18(:(vuu3000, vuu3001), :(vuu31000, vuu31001), eh) → new_asAs(new_esEs20(vuu3000, vuu31000, eh), new_esEs18(vuu3001, vuu31001, eh))
new_span2Zs11(vuu3110, vuu3111, True, ba) → new_span2Zs12(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_primMulNat0(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Float) → new_esEs12(vuu3002, vuu31002)
new_span2Ys3(vuu9, :(vuu110, vuu111), bb) → new_span2Ys14(vuu9, vuu110, vuu111, new_esEs4(Just(vuu9), vuu110, bb), bb)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs6(vuu300, vuu3100)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, fc)) → new_esEs4(vuu3000, vuu31000, fc)
new_esEs10(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs21(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_Either, hf), hg), fb) → new_esEs19(vuu3000, vuu31000, hf, hg)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs7(vuu3000, vuu31000)
new_primPlusNat0(Zero, vuu3100100) → Succ(vuu3100100)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, ec)) → new_esEs14(vuu300, vuu3100, ec)
new_span2Zs3(vuu18, [], bc) → []
new_span2Zs12(vuu3110, vuu3111, vuu48, vuu47, ba) → vuu47
new_groupByZs0(Nothing, :(Just(vuu3100), vuu311), ba) → :(Just(vuu3100), vuu311)
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Int) → new_esEs7(vuu3002, vuu31002)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Double, fb) → new_esEs6(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bbb)) → new_esEs4(vuu3000, vuu31000, bbb)
new_sr(Pos(vuu30010), Neg(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_sr(Neg(vuu30010), Pos(vuu310010)) → Neg(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, fh)) → new_esEs14(vuu3000, vuu31000, fh)
new_esEs24(vuu3001, vuu31001, app(app(ty_Either, bdd), bde)) → new_esEs19(vuu3001, vuu31001, bdd, bde)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_span2Zs3(vuu18, :(vuu200, vuu201), bc) → new_span2Zs14(vuu18, vuu200, vuu201, new_esEs4(Just(vuu18), vuu200, bc), bc)
new_esEs5(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs13(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), ee, ef, eg) → new_asAs(new_esEs23(vuu3000, vuu31000, ee), new_asAs(new_esEs24(vuu3001, vuu31001, ef), new_esEs25(vuu3002, vuu31002, eg)))
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Ratio, hb), fb) → new_esEs14(vuu3000, vuu31000, hb)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, ed)) → new_esEs4(vuu300, vuu3100, ed)
new_esEs9(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs15(LT, GT) → False
new_esEs15(GT, LT) → False
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Float, fb) → new_esEs12(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_[], ce)) → new_esEs18(vuu3000, vuu31000, ce)
new_span2Zs14(vuu18, vuu200, vuu201, False, bc) → :(vuu200, vuu201)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs24(vuu3001, vuu31001, app(ty_Ratio, bch)) → new_esEs14(vuu3001, vuu31001, bch)
new_esEs4(Nothing, Nothing, ed) → True
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bfh), bga)) → new_esEs19(vuu3000, vuu31000, bfh, bga)
new_esEs10(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, bd), be)) → new_esEs8(vuu300, vuu3100, bd, be)
new_esEs18([], :(vuu31000, vuu31001), eh) → False
new_esEs18(:(vuu3000, vuu3001), [], eh) → False
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs15(LT, LT) → True
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, ee), ef), eg)) → new_esEs13(vuu300, vuu3100, ee, ef, eg)
new_esEs11(@0, @0) → True
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_@0) → new_esEs11(vuu3002, vuu31002)
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bfa), bfb), bfc)) → new_esEs13(vuu3000, vuu31000, bfa, bfb, bfc)
new_span2Ys12(vuu3110, vuu3111, True, ba) → new_span2Ys13(vuu3110, vuu3111, new_span2Ys2(vuu3111, ba), new_span2Zs2(vuu3111, ba), ba)
new_span2Zs14(vuu18, vuu200, vuu201, True, bc) → new_span2Zs13(vuu18, vuu200, vuu201, new_span2Ys3(vuu18, vuu201, bc), new_span2Zs3(vuu18, vuu201, bc), bc)
new_esEs12(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs10(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_span2Ys13(vuu3110, vuu3111, vuu46, vuu45, ba) → :(vuu3110, vuu46)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs15(vuu300, vuu3100)
new_groupByZs00(vuu18, vuu19, vuu20, True, bc) → new_span2Zs3(vuu18, vuu20, bc)
new_esEs24(vuu3001, vuu31001, ty_Int) → new_esEs7(vuu3001, vuu31001)
new_esEs16(True, True) → True
new_esEs10(vuu3001, vuu31001, ty_Char) → new_esEs17(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_esEs25(vuu3002, vuu31002, app(ty_Ratio, beb)) → new_esEs14(vuu3002, vuu31002, beb)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bbg), bbh)) → new_esEs8(vuu3000, vuu31000, bbg, bbh)
new_esEs10(vuu3001, vuu31001, ty_@0) → new_esEs11(vuu3001, vuu31001)
new_esEs15(LT, EQ) → False
new_esEs15(EQ, LT) → False
new_esEs20(vuu3000, vuu31000, app(ty_[], gc)) → new_esEs18(vuu3000, vuu31000, gc)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(app(ty_@3, baa), bab), bac)) → new_esEs13(vuu3000, vuu31000, baa, bab, bac)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(ty_Either, cf), cg)) → new_esEs19(vuu3000, vuu31000, cf, cg)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Bool) → new_esEs16(vuu3002, vuu31002)
new_span2Ys11(vuu9, vuu110, vuu111, vuu50, vuu49, bb) → :(vuu110, vuu50)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(ty_Either, bah), bba)) → new_esEs19(vuu3000, vuu31000, bah, bba)
new_esEs15(EQ, GT) → False
new_esEs15(GT, EQ) → False
new_groupByZs0(vuu30, [], ba) → []
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs10(vuu3001, vuu31001, ty_Float) → new_esEs12(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(ty_Ratio, cb)) → new_esEs14(vuu3000, vuu31000, cb)
new_sr(Neg(vuu30010), Neg(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(app(ty_Either, bef), beg)) → new_esEs19(vuu3002, vuu31002, bef, beg)
new_asAs(False, vuu40) → False
new_sr(Pos(vuu30010), Pos(vuu310010)) → Pos(new_primMulNat0(vuu30010, vuu310010))
new_groupByZs0(Nothing, :(Nothing, vuu311), ba) → new_span2Zs2(vuu311, ba)
new_primEqNat0(Zero, Zero) → True
new_esEs10(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Char, fb) → new_esEs17(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300100), Zero) → Zero
new_primMulNat0(Zero, Succ(vuu3100100)) → Zero
new_esEs19(Right(vuu3000), Left(vuu31000), fa, fb) → False
new_esEs19(Left(vuu3000), Right(vuu31000), fa, fb) → False
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs17(vuu300, vuu3100)
new_esEs18([], [], eh) → True
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bcb), bcc)) → new_esEs19(vuu3000, vuu31000, bcb, bcc)
new_esEs25(vuu3002, vuu31002, app(ty_[], bee)) → new_esEs18(vuu3002, vuu31002, bee)
new_esEs10(vuu3001, vuu31001, app(app(ty_@2, df), dg)) → new_esEs8(vuu3001, vuu31001, df, dg)
new_esEs9(vuu3000, vuu31000, app(ty_Maybe, bf)) → new_esEs4(vuu3000, vuu31000, bf)
new_esEs4(Just(vuu3000), Just(vuu31000), app(ty_[], bfg)) → new_esEs18(vuu3000, vuu31000, bfg)
new_esEs7(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs24(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs24(vuu3001, vuu31001, app(ty_[], bdc)) → new_esEs18(vuu3001, vuu31001, bdc)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bbc), bbd), bbe)) → new_esEs13(vuu3000, vuu31000, bbc, bbd, bbe)
new_esEs24(vuu3001, vuu31001, ty_Ordering) → new_esEs15(vuu3001, vuu31001)
new_esEs22(vuu3001, vuu31001, ty_Integer) → new_esEs5(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, ga), gb)) → new_esEs8(vuu3000, vuu31000, ga, gb)
new_span2Zs2(:(vuu3110, vuu3111), ba) → new_span2Zs11(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs16(vuu300, vuu3100)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Ordering, fb) → new_esEs15(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, ty_@0) → new_esEs11(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs7(vuu300, vuu3100)
new_span2Ys12(vuu3110, vuu3111, False, ba) → []
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs5(vuu300, vuu3100)
new_esEs10(vuu3001, vuu31001, ty_Bool) → new_esEs16(vuu3001, vuu31001)
new_primPlusNat0(Succ(vuu530), vuu3100100) → Succ(Succ(new_primPlusNat1(vuu530, vuu3100100)))
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(app(ty_@2, bae), baf)) → new_esEs8(vuu3000, vuu31000, bae, baf)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_@0, fb) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs6(vuu3000, vuu31000)
new_span2Zs11(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_esEs16(False, False) → True
new_esEs25(vuu3002, vuu31002, app(app(app(ty_@3, bdg), bdh), bea)) → new_esEs13(vuu3002, vuu31002, bdg, bdh, bea)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs24(vuu3001, vuu31001, ty_Double) → new_esEs6(vuu3001, vuu31001)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(ty_@2, hc), hd), fb) → new_esEs8(vuu3000, vuu31000, hc, hd)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_Maybe, gf), fb) → new_esEs4(vuu3000, vuu31000, gf)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, fa), fb)) → new_esEs19(vuu300, vuu3100, fa, fb)
new_esEs8(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bd, be) → new_asAs(new_esEs9(vuu3000, vuu31000, bd), new_esEs10(vuu3001, vuu31001, be))
new_esEs25(vuu3002, vuu31002, app(app(ty_@2, bec), bed)) → new_esEs8(vuu3002, vuu31002, bec, bed)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Bool, fb) → new_esEs16(vuu3000, vuu31000)
new_esEs9(vuu3000, vuu31000, app(app(app(ty_@3, bg), bh), ca)) → new_esEs13(vuu3000, vuu31000, bg, bh, ca)
new_primPlusNat1(Succ(vuu5300), Zero) → Succ(vuu5300)
new_primPlusNat1(Zero, Succ(vuu31001000)) → Succ(vuu31001000)
new_esEs10(vuu3001, vuu31001, app(ty_[], dh)) → new_esEs18(vuu3001, vuu31001, dh)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, gd), ge)) → new_esEs19(vuu3000, vuu31000, gd, ge)
new_esEs9(vuu3000, vuu31000, ty_Int) → new_esEs7(vuu3000, vuu31000)
new_esEs16(False, True) → False
new_esEs16(True, False) → False
new_span2Zs2([], ba) → []
new_esEs6(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs7(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_span2Ys14(vuu9, vuu110, vuu111, True, bb) → new_span2Ys11(vuu9, vuu110, vuu111, new_span2Ys3(vuu9, vuu111, bb), new_span2Zs3(vuu9, vuu111, bb), bb)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(app(ty_@3, bce), bcf), bcg)) → new_esEs13(vuu3001, vuu31001, bce, bcf, bcg)
new_esEs4(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs5(vuu3000, vuu31000)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_esEs10(vuu3001, vuu31001, app(app(ty_Either, ea), eb)) → new_esEs19(vuu3001, vuu31001, ea, eb)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, fd), ff), fg)) → new_esEs13(vuu3000, vuu31000, fd, ff, fg)
new_esEs10(vuu3001, vuu31001, app(ty_Ratio, de)) → new_esEs14(vuu3001, vuu31001, de)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Int, fb) → new_esEs7(vuu3000, vuu31000)
new_esEs19(Left(vuu3000), Left(vuu31000), app(ty_[], he), fb) → new_esEs18(vuu3000, vuu31000, he)
new_esEs19(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, gg), gh), ha), fb) → new_esEs13(vuu3000, vuu31000, gg, gh, ha)
new_esEs26(vuu300, vuu3100, app(ty_[], eh)) → new_esEs18(vuu300, vuu3100, eh)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs25(vuu3002, vuu31002, ty_Double) → new_esEs6(vuu3002, vuu31002)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs11(vuu300, vuu3100)
new_span2Ys3(vuu9, [], bb) → []
new_span2Ys2([], ba) → []
new_asAs(True, vuu40) → vuu40
new_primMulNat0(Succ(vuu300100), Succ(vuu3100100)) → new_primPlusNat0(new_primMulNat0(vuu300100, Succ(vuu3100100)), vuu3100100)
new_esEs9(vuu3000, vuu31000, ty_Bool) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, app(ty_Maybe, bdf)) → new_esEs4(vuu3002, vuu31002, bdf)
new_groupByZs0(Just(vuu300), :(Just(vuu3100), vuu311), ba) → new_groupByZs00(vuu300, vuu3100, vuu311, new_esEs26(vuu300, vuu3100, ba), ba)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Float) → new_esEs12(vuu3000, vuu31000)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs25(vuu3002, vuu31002, ty_Integer) → new_esEs5(vuu3002, vuu31002)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3001, vuu31001, app(app(ty_@2, bda), bdb)) → new_esEs8(vuu3001, vuu31001, bda, bdb)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbf)) → new_esEs14(vuu3000, vuu31000, bbf)
new_span2Ys2(:(vuu3110, vuu3111), ba) → new_span2Ys12(vuu3110, vuu3111, new_esEs4(Nothing, vuu3110, ba), ba)
new_esEs15(GT, GT) → True
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs15(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bca)) → new_esEs18(vuu3000, vuu31000, bca)
new_esEs9(vuu3000, vuu31000, ty_Char) → new_esEs17(vuu3000, vuu31000)
new_esEs25(vuu3002, vuu31002, ty_Ordering) → new_esEs15(vuu3002, vuu31002)
new_esEs19(Right(vuu3000), Right(vuu31000), fa, app(ty_Maybe, hh)) → new_esEs4(vuu3000, vuu31000, hh)
new_esEs19(Left(vuu3000), Left(vuu31000), ty_Integer, fb) → new_esEs5(vuu3000, vuu31000)
new_span2Ys14(vuu9, vuu110, vuu111, False, bb) → []
new_span2Zs13(vuu18, vuu200, vuu201, vuu52, vuu51, bc) → vuu51
new_groupByZs00(vuu18, vuu19, vuu20, False, bc) → :(Just(vuu19), vuu20)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_esEs4(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bfe), bff)) → new_esEs8(vuu3000, vuu31000, bfe, bff)
new_esEs10(vuu3001, vuu31001, app(ty_Maybe, da)) → new_esEs4(vuu3001, vuu31001, da)
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_groupByZs0(Just(vuu300), :(Nothing, vuu311), ba) → :(Nothing, vuu311)

The set Q consists of the following terms:

new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs9(x0, x1, ty_Bool)
new_esEs18(:(x0, x1), [], x2)
new_esEs4(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_span2Ys3(x0, [], x1)
new_primMulNat0(Succ(x0), Zero)
new_esEs4(Nothing, Nothing, x0)
new_esEs9(x0, x1, app(ty_Ratio, x2))
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Int)
new_esEs18([], [], x0)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_span2Zs11(x0, x1, True, x2)
new_esEs26(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, x4, x5)
new_groupByZs0(x0, [], x1)
new_esEs25(x0, x1, ty_@0)
new_esEs25(x0, x1, ty_Char)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs22(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Bool)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_groupByZs0(Nothing, :(Nothing, x0), x1)
new_esEs19(Left(x0), Right(x1), x2, x3)
new_esEs19(Right(x0), Left(x1), x2, x3)
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Int)
new_esEs4(Just(x0), Just(x1), ty_Ordering)
new_esEs9(x0, x1, ty_Float)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), ty_@0, x2)
new_esEs11(@0, @0)
new_sr(Neg(x0), Neg(x1))
new_esEs10(x0, x1, ty_Char)
new_esEs25(x0, x1, ty_Int)
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Right(x0), Right(x1), x2, ty_Char)
new_esEs19(Left(x0), Left(x1), ty_Char, x2)
new_esEs18(:(x0, x1), :(x2, x3), x4)
new_esEs25(x0, x1, ty_Integer)
new_esEs10(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs9(x0, x1, app(app(ty_@2, x2), x3))
new_esEs14(:%(x0, x1), :%(x2, x3), x4)
new_esEs19(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Integer(x0), Integer(x1))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_span2Zs11(x0, x1, False, x2)
new_esEs10(x0, x1, app(ty_Maybe, x2))
new_esEs13(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_span2Ys12(x0, x1, False, x2)
new_esEs24(x0, x1, ty_Char)
new_esEs12(Float(x0, x1), Float(x2, x3))
new_esEs4(Just(x0), Just(x1), ty_Double)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Double)
new_span2Ys3(x0, :(x1, x2), x3)
new_esEs16(True, False)
new_esEs16(False, True)
new_esEs4(Just(x0), Just(x1), ty_Bool)
new_esEs9(x0, x1, app(ty_Maybe, x2))
new_esEs17(Char(x0), Char(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_span2Ys14(x0, x1, x2, True, x3)
new_esEs4(Just(x0), Just(x1), app(ty_[], x2))
new_esEs21(x0, x1, ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs19(Left(x0), Left(x1), ty_Int, x2)
new_esEs9(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), ty_Ordering, x2)
new_span2Ys12(x0, x1, True, x2)
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs16(True, True)
new_esEs4(Just(x0), Just(x1), ty_Integer)
new_esEs24(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Double)
new_groupByZs0(Just(x0), :(Just(x1), x2), x3)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_span2Zs2([], x0)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs10(x0, x1, ty_Double)
new_esEs19(Left(x0), Left(x1), ty_Double, x2)
new_primEqNat0(Zero, Zero)
new_esEs4(Just(x0), Just(x1), ty_Int)
new_esEs19(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_span2Zs13(x0, x1, x2, x3, x4, x5)
new_esEs10(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Int)
new_span2Ys2(:(x0, x1), x2)
new_sr(Pos(x0), Pos(x1))
new_esEs15(GT, GT)
new_esEs19(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs9(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_span2Ys2([], x0)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs7(x0, x1)
new_esEs15(LT, GT)
new_esEs15(GT, LT)
new_esEs19(Right(x0), Right(x1), x2, ty_Integer)
new_groupByZs00(x0, x1, x2, False, x3)
new_primMulNat0(Zero, Zero)
new_esEs16(False, False)
new_esEs25(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Bool)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_groupByZs0(Just(x0), :(Nothing, x1), x2)
new_esEs4(Just(x0), Just(x1), ty_Float)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_span2Zs14(x0, x1, x2, True, x3)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_Bool)
new_esEs24(x0, x1, ty_@0)
new_esEs4(Just(x0), Nothing, x1)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Bool)
new_span2Ys13(x0, x1, x2, x3, x4)
new_esEs23(x0, x1, ty_Integer)
new_primPlusNat1(Zero, Succ(x0))
new_primMulNat0(Zero, Succ(x0))
new_span2Ys14(x0, x1, x2, False, x3)
new_esEs10(x0, x1, ty_Bool)
new_esEs19(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(Left(x0), Left(x1), ty_Float, x2)
new_esEs15(EQ, EQ)
new_esEs25(x0, x1, ty_Float)
new_esEs10(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(x0, x1, app(ty_Ratio, x2))
new_groupByZs00(x0, x1, x2, True, x3)
new_esEs10(x0, x1, ty_Integer)
new_primEqNat0(Succ(x0), Zero)
new_esEs4(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs19(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_span2Zs12(x0, x1, x2, x3, x4)
new_esEs10(x0, x1, ty_@0)
new_primPlusNat0(Zero, x0)
new_esEs10(x0, x1, app(app(ty_@2, x2), x3))
new_esEs4(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_Ordering)
new_esEs26(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_Ordering)
new_esEs18([], :(x0, x1), x2)
new_esEs10(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs9(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs19(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(x0, x1, ty_Float)
new_esEs26(x0, x1, ty_@0)
new_esEs23(x0, x1, ty_Double)
new_esEs9(x0, x1, ty_@0)
new_esEs4(Just(x0), Just(x1), ty_Char)
new_esEs19(Right(x0), Right(x1), x2, app(ty_[], x3))
new_span2Zs2(:(x0, x1), x2)
new_esEs19(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs20(x0, x1, ty_Bool)
new_esEs24(x0, x1, ty_Ordering)
new_esEs4(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs24(x0, x1, ty_Double)
new_esEs4(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs19(Right(x0), Right(x1), x2, ty_@0)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs19(Left(x0), Left(x1), ty_Bool, x2)
new_esEs25(x0, x1, ty_Ordering)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs9(x0, x1, ty_Ordering)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs4(Just(x0), Just(x1), ty_@0)
new_esEs4(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs19(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_span2Zs14(x0, x1, x2, False, x3)
new_esEs23(x0, x1, ty_Float)
new_esEs24(x0, x1, ty_Int)
new_esEs19(Left(x0), Left(x1), ty_Integer, x2)
new_esEs19(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs15(EQ, LT)
new_esEs15(LT, EQ)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs20(x0, x1, ty_Ordering)
new_primPlusNat1(Succ(x0), Zero)
new_primPlusNat0(Succ(x0), x1)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs9(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_groupByZs0(Nothing, :(Just(x0), x1), x2)
new_esEs15(LT, LT)
new_esEs19(Right(x0), Right(x1), x2, ty_Float)
new_esEs20(x0, x1, ty_Int)
new_esEs9(x0, x1, ty_Double)
new_asAs(False, x0)
new_esEs10(x0, x1, ty_Ordering)
new_span2Zs3(x0, :(x1, x2), x3)
new_esEs15(GT, EQ)
new_esEs15(EQ, GT)
new_esEs19(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_span2Zs3(x0, [], x1)
new_esEs9(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(Double(x0, x1), Double(x2, x3))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.